/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

/**
 * NuGat-API named Chameleon developed by Simon De Baets to Verimag.
 *
 */


package chameleon.model.NuGatStructure.fsm;

import chameleon.model.NuGatStructure.bdd.Bdd;
import chameleon.model.NuGatStructure.bdd.BddTrans;
import chameleon.model.NuGatStructure.enc.BddEnc;
import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.NuGatStructure.utils.Node;
import chameleon.model.NuGatStructure.NuGatStructure;
import chameleon.model.NuGatStructure.prop.Prop;
import chameleon.model.NuGatStructure.prop.PropDbGame;
import com.sun.jna.Pointer;

/**
 * This class is a wrapper to the C struct BddFsm.c
 *
 * @author simon
 */
public class BddFsm extends NuGatStructure {

    public BddFsm (Pointer structure, NuGatInterface nugat){
        super (structure, nugat);
    }
    
    
    public BddFsm (BddEnc encoding,
                   Bdd initStates,
                   Bdd invarStates,
                   Bdd invarInputs,
                   BddTrans trans,
                   Pointer justice,
                   Pointer compassion,
                   NuGatInterface nugat){
        super (nugat.BddFsm_create(encoding.ptr(),
                initStates.ptr(),
                invarStates.ptr(),
                invarInputs.ptr(),
                trans.ptr(),
                justice,
                compassion),nugat);
    }

    
    @Override
    public BddFsm clone(){
        return new BddFsm(nugat_.BddFsm_copy(this.ptr()),nugat_);
    }
    
    /**
     * Return the transtion relation to this bddFsm. This is not a clone, so 
     * do not destroy it.
     *
     * @return BddTrans_ptr
     */

    public BddTrans getTrans(){
        /*FsmBuilder fsmBuilder = new FsmBuilder(nugat_.Compile_get_global_fsm_builder(),
                nugat_);
        BddEnc enc = this.getBddEncoding();
        DdManager ddManager = enc.getDdManager();
        ClusterList clusters;
        ClusterOptions clusterOptions;
        Opt opt = new Opt (nugat_.OptsHandler_get_instance(), nugat_);
        
        Node transExpr = enc.bddToExpr(this.getMonolithicTransBdd());
        
        
        /* clusters construction */
        /*clusters = fsmBuilder.clusterizeExpr(
                enc,
                transExpr.ptr());
        
        clusterOptions = new ClusterOptions(nugat_.OptsHandler_get_instance(), nugat_);
        
        
        BddTrans trans = new BddTrans(ddManager,
                                clusters,
                                enc.getStateVarsCube(),
                                ddManager.bddOne(),
                                enc.getNextStateVarsCube(),
                                opt.getPartitionMethod(),
                                clusterOptions,
                                nugat_);
        
        return trans;*/
        return new BddTrans (nugat_.BddFsm_get_trans(this.ptr()),nugat_);
    }
    
    
    /**Function********************************************************************

       Synopsis           [Getter for justice list]

       Description        [self keeps the ownership of the returned object]

       SideEffects        []

       SeeAlso            []

    ******************************************************************************/
    
    public Pointer getJustice(){
        return nugat_.BddFsm_get_justice(this.ptr());
    }
    
    /**Function********************************************************************

       Synopsis           [Getter for compassion list]

       Description        [self keeps the ownership of the returned object]

       SideEffects        []

       SeeAlso            []

    ******************************************************************************/
    
    public Pointer getCompassion(){
        return nugat_.BddFsm_get_compassion(this.ptr());
    }
    
    /**Function********************************************************************

       Synopsis           [Getter for state constraints]

       Description        [Returned bdd is referenced]

       SideEffects        []

       SeeAlso            []

    ******************************************************************************/
    
    public Bdd getInvarStates(){
        return new Bdd(nugat_.BddFsm_get_state_constraints(this.ptr()),nugat_);
    }
    
    /**Function********************************************************************

       Synopsis           [Getter for input constraints]

       Description        [Returned bdd is referenced]

       SideEffects        []

       SeeAlso            []

    ******************************************************************************/
    
    public Bdd getInvarInputs(){
        return new Bdd(nugat_.BddFsm_get_input_constraints(this.ptr()),nugat_);
    }

    
    public BddEnc getBddEncoding(){
        return new BddEnc(nugat_.BddFsm_get_bdd_encoding(this.ptr()),nugat_);
    }
    
    /**Function********************************************************************

       Synopsis           [Getter for init]

       Description        [Returned bdd is referenced]

       SideEffects        []

       SeeAlso            []

    ******************************************************************************/
    
    public Bdd getInitStates(){
        return new Bdd(nugat_.BddFsm_get_init(this.ptr()),nugat_);
    }
    
    /**Function********************************************************************

       Synopsis     [Returns a bdd that represents the monolithic
       transition relation]

       Description  [This method returns a monolithic representation of
       the transition relation, which is computed on the
       basis of the internal partitioned representation by
       composing all the element of the partition.

       Returned bdd is referenced.]

       SideEffects  [Internal cache could change]

       SeeAlso      []

    ******************************************************************************/
    
    public Bdd getMonolithicTransBdd(){
        return new Bdd (nugat_.BddFsm_get_monolithic_trans_bdd(this.ptr()),nugat_);
    }
    
    /**Function********************************************************************

       Synopsis    [Variant of
                    BddFsm_apply_synchronous_product_custom_varsets that
                    simply takes all variables in the encoding into
                    account.]

       Description [The result goes into self, no changes on other. Both
                    the two FSMs must be based on the same dd manager.
                    The cache will change, since a new separated family
                    will be created for the internal cache, and it will
                    not be shared anymore with previous family.  From the
                    old cache will be reused as much as possible]

       SideEffects [self will change]

       SeeAlso     [BddFsm_apply_synchronous_product_custom_varsets,
                    BddFsmCache_reset_not_reusable_fields_after_product]

    ******************************************************************************/
    
    public void applySynchronousProduct(BddFsm other){
        nugat_.BddFsm_apply_synchronous_product(this.ptr(), other.ptr());
    }

    /**
     * Check if the current FSM repsect the ltl property given on input
     * @param ltlSpec 
     */    
    public void checkLtlSpec(Prop ltlSpec, PropDbGame propDbGame){
        
        BddEnc enc = this.getBddEncoding();
        BddFsm nusmvBddFsm = new BddFsm(enc,
                this.getInitStates(),
                this.getInvarStates(),
                this.getInvarInputs(),
                this.getTrans(),
                nugat_.JusticeList_create(enc.getDdManager().ptr()),
                nugat_.CompassionList_create(enc.getDdManager().ptr()),
                nugat_);
        
        propDbGame.setBddFsm(nusmvBddFsm);
        
        //set Sexp Fsm
            
         GameSexpFsm gameSexpFsm = new GameSexpFsm( propDbGame.getGameScalarSexpFsm(), nugat_);
        
        ltlSpec.setScalarSexpFsm(gameSexpFsm.getPlayer1());
        ltlSpec.setBddFsm(nusmvBddFsm);
        
        nugat_.Chameleon_Ltl_CheckLtlSpec(ltlSpec.ptr());
        ltlSpec.setBddFsm(new BddFsm(Pointer.NULL, nugat_));
    }

    public void printInfo(String file){
        nugat_.BddFsm_print_info(this.ptr(), nugat_.CmdOpenFile(file));
    }

    public String monolithicTransToString(){
        Bdd trans = getMonolithicTransBdd();
        BddEnc enc = getBddEncoding();
        Node expr = enc.bddToExpr(trans);
        return expr.sprintNode();
    }
}
